// 
// File:   prism_parser.h
// Author: cionescu
//
// Created on 8 January 2007, 12:46
//

#ifndef _prism_parser_H
#define	_prism_parser_H
#define PHOENIX_LIMIT 6
#define BOOST_SPIRIT_CLOSURE_LIMIT 6
#define BOOST_SPIRIT_DEBUG
#define BOOST_SPIRIT_DEBUG_RULES
#define BOOST_SPIRIT_DEBUG_NODES

#include <boost/spirit/core.hpp>
#include <boost/spirit/attribute.hpp>
#include <vector>
#include <boost/spirit/phoenix/primitives.hpp>
#include <boost/spirit/phoenix/operators.hpp>
#include <boost/spirit/phoenix/functions.hpp>
#include <boost/spirit/phoenix.hpp>

#include "prism_actions.h"
#include "prism_token_parser.h"
#include "prism_tokens.h"
#include "prism_ast.h"
#include "prism_constants.h"

using namespace std;
using namespace phoenix;
using namespace boost::spirit;

typedef vector<token*>::const_iterator token_iterator_t;
typedef prism_ast_transition::transition_type transition_type;
typedef prism_ast_transition::transition_element_type transition_element_type;

void print_token(const token* t) {
    clog<<"token:"<<endl;
    t->print_token();
}

void print_rule(const token_iterator_t begin, const token_iterator_t end) {
    clog<<"rule:"<<endl;
    for (token_iterator_t it = begin; it!=end; it++)
    (*it)->print_token();
}

struct populate_impl{
  template <typename Container, typename Item>
  struct result{
    typedef void type;
  };

  template <typename Container, typename Item>
  void operator()(Container& c, Item const& item) const{
    c.populate(item);
  }
};

struct insert_impl{
  template <typename Container, typename Item>
  struct result{
    typedef void type;
  };

  template <typename Container, typename Item>
  void operator()(Container& c, Item const& item) const{
    c.insert(item);
  }
};

struct push_back_impl{
  template <typename Container, typename Item>
  struct result{
    typedef void type;
  };

  template <typename Container, typename Item>
  void operator()(Container& c, Item const& item) const{
    c.push_back(item);
  }
};

function<insert_impl> const insert = insert_impl();
function<push_back_impl> const push_back = push_back_impl();

////////////////////////////// closures
struct dtmc_closure : boost::spirit::closure<dtmc_closure, prism_ast_expr, vector<prism_ast_formula>, vector<prism_ast_variable>, vector<prism_ast_expr> , vector<prism_ast_module>, prism_ast_variable> {
  member1 res;
  member2 form;
  member3 vars;
  member4 init;
  member5 modules;
  member6 vartmp;
};

struct variable_closure : boost::spirit::closure<variable_closure, token*, prism_ast_expr, prism_ast_variable> {
  member1 name;
  member2 min;
  //member3 var;
};

struct module_closure : boost::spirit::closure<module_closure, token* , vector<prism_ast_variable>, vector<prism_ast_transition>, vector<prism_ast_expr> > {
  member1 name;
  member2 variables;
  member3 transitions;
  member4 init;
};

struct transition_closure : boost::spirit::closure<transition_closure, prism_ast_expr, transition_type, token*> {
  member1 from;
  member2 to;
  member3 label;
};

struct updates_closure : boost::spirit::closure<updates_closure, prism_ast_expr, prism_ast_update::update_type> {
  member1 prob;
  member2 upds;
};

struct update_closure : boost::spirit::closure<update_closure, token*> {
  member1 name;
};

struct binexp_closure : boost::spirit::closure<binexp_closure, prism_ast_expr, int, prism_ast_expr> {
    member1         left;
    member2         op;
    member3         res;
};

/**
This is the parser for the prism language.

It uses advanced features of SPIRIT like closures to extract the context
information necessary for the parse and generates the AST. The AST is not
the default one generated by SPIRIT with ast_parse but a custom made AST. 
This will hopefully render the manipulations related to the semantic analysis, 
state space generation and simulation significatly easier to implement.

TODO: formula expressions, functions (pow, exp, max,...)
*/
template<typename Actions>
struct prism_parser : public grammar<prism_parser<Actions> > {    
    
    prism_parser(Actions& a) 
            : m_actions(a){
    }
        
    template <typename ScannerT>
    struct definition {
        
        definition(prism_parser const& self)
            :MODULE(self.m_actions.m_symbol_table["module"]),
             ENDMODULE(self.m_actions.m_symbol_table["endmodule"]),
             INIT(self.m_actions.m_symbol_table["init"]),
             ENDINIT(self.m_actions.m_symbol_table["endinit"]),
             CONST(self.m_actions.m_symbol_table["const"]),
             COLON(self.m_actions.m_symbol_table[":"]), 
             LBRAKET(self.m_actions.m_symbol_table["["]),
             RBRAKET(self.m_actions.m_symbol_table["]"]),
             LPAR(self.m_actions.m_symbol_table["("]),
             RPAR(self.m_actions.m_symbol_table[")"]),
             DOTS(self.m_actions.m_symbol_table[".."]),
             BOOL(self.m_actions.m_symbol_table["bool"]),
             ARROW(self.m_actions.m_symbol_table["->"]),
             AND(self.m_actions.m_symbol_table["&"]),
             PRIME(self.m_actions.m_symbol_table["'"]),
             EQ(self.m_actions.m_symbol_table["="]),
             NEQ(self.m_actions.m_symbol_table["!="]),
             TRUE(self.m_actions.m_symbol_table["true"]),
             OR(self.m_actions.m_symbol_table["|"]),
             NOT(self.m_actions.m_symbol_table["!"]),
             LT(self.m_actions.m_symbol_table["<"]),
             GR(self.m_actions.m_symbol_table[">"]),
             LTEQ(self.m_actions.m_symbol_table["<="]),
             GREQ(self.m_actions.m_symbol_table[">="]),
             PLUS(self.m_actions.m_symbol_table["+"]),
             MINUS(self.m_actions.m_symbol_table["-"]),
             MULT(self.m_actions.m_symbol_table["*"]),
             DIV(self.m_actions.m_symbol_table["/"]),
             SEMICOLON(self.m_actions.m_symbol_table[";"]),
             FORMULA(self.m_actions.m_symbol_table["formula"]),
             SYSTEM(self.m_actions.m_symbol_table["system"]),
             ENDSYSTEM(self.m_actions.m_symbol_table["endsystem"]),
             BAR(self.m_actions.m_symbol_table["|"]) {
            
               typedef prism_ast_update::update_type update_type;
               typedef prism_ast_transition::transition_type transition_type;
               typedef prism_ast_update::update_element_type update_element_type;
               typedef prism_ast_variable::variable_constraint variable_constraint;
               
                Actions& act = self.m_actions;
                prism_ast_program prog = act.m_ast;
                                
                // A module definition consists of a module, a sequence of 
                // variable definitions and a sequence of transitions
                
                dtmc
                = *(
                    formula_def
                  | INIT >> *(variable_def[push_back(dtmc.vars, dtmc.vartmp)] )>> ENDINIT
                  | module_def
                  | sysmodule
                    )
                ;
                  
                // todo system composition
                sysmodule
                = SYSTEM >> ENDSYSTEM;
                
                module_def
    		=       
                        MODULE
                    >>  ident_p [module_def.name = arg1][module_def.variables = construct_<vector<prism_ast_variable> >()]
                    >> *( variable_def[push_back(module_def.variables, dtmc.vartmp)] )
                    >> *( transition_def )
                    >>  ENDMODULE [push_back(dtmc.modules, construct_<prism_ast_module>(module_def.name, module_def.variables, module_def.transitions))]
                ;

    		variable_def
    		= (     
                        ident_p[variable_def.name = arg1]
    		    >>  COLON
                    >>  LBRAKET [dtmc.vartmp=construct_<prism_ast_variable>(variable_def.name,1)]
                    >>  expression [variable_def.min = dtmc.res]
                    >>  DOTS
                    >>  expression [push_back(dtmc.vartmp , construct_<variable_constraint>(variable_def.min, dtmc.res))]
                    >>  RBRAKET
                    >>  (( INIT >> expression ) 
                        | eps_p ) 
                    >>  SEMICOLON
                    )
                  | (   ident_p [variable_def.name = arg1]
                    >>  COLON
                    >>  BOOL [dtmc.vartmp=construct_<prism_ast_variable>(variable_def.name,0)]
                    >>  ((INIT >> expression )
                        | eps_p) 
                    >>  SEMICOLON
                    )
    		;
                
    				
    		transition_def
    		=
                        LBRAKET
                    >>  ( ident_p [transition_def.label = arg1]
                        | eps_p )
                    >>  RBRAKET
                    >>  expression[transition_def.from = dtmc.res]
                                  [transition_def.to=construct_<transition_type>()]
                    >>  ARROW
                    >>  updates[push_back(module_def.transitions, construct_<prism_ast_transition>(transition_def.label, transition_def.from, transition_def.to))]
                    >>  SEMICOLON
    		;
    			
    		updates
    		=       ( expression[updates.prob = dtmc.res]
                    >>  COLON[updates.upds=construct_<update_type>()]
                    >>  update[push_back(transition_def.to, construct_<transition_element_type>(updates.prob, construct_<prism_ast_update>(updates.upds)))]
                    >>  *( PLUS
                        >>  expression[updates.prob = dtmc.res]
                        >>  COLON[updates.upds=construct_<update_type>()]
                        >>  update[push_back(transition_def.to, construct_<transition_element_type>(updates.prob, construct_<prism_ast_update>(updates.upds)))]
                        ) ) 
                    /*|   (eps_p //[updates.prob = NULL]
                              [updates.upds=construct_<update_type>()]
                        >> update [push_back(transition_def.to, construct_<transition_element_type>(updates.prob, construct_<prism_ast_update>(updates.upds)))]
                        )*/
    		;
    				
    		update 
    		= (     LPAR
                    >>  ident_p[update.name = arg1]
                    >>  PRIME
                    >>  EQ          // TODO
                    >>  expression[insert(updates.upds, construct_<update_element_type>( update.name, dtmc.res))]
                    >>  RPAR
                    ) >> *( AND >> update
                            )
    		;               
                
    		expression
    		=   binexp[expression.left = dtmc.res]
                    >> *(( OR[expression.op = PRISM_OP_OR] >> binexp[dtmc.res = construct_<prism_ast_binexpr>(expression.op, expression.left, dtmc.res)] )
                        |( AND[expression.op = PRISM_OP_AND] >> binexp[dtmc.res = construct_<prism_ast_binexpr>(expression.op, expression.left, dtmc.res)] )
                        )
                ;
    				
    		binexp
    		=   numexp[binexp.left = dtmc.res]
                    >> !( (EQ[binexp.op = PRISM_OP_EQ] >> numexp[dtmc.res = construct_<prism_ast_binexpr>(binexp.op, binexp.left, dtmc.res)]) 
                      | ( NEQ[binexp.op = PRISM_OP_NEQ] >> numexp[dtmc.res = construct_<prism_ast_binexpr>(binexp.op, binexp.left, dtmc.res)]) 
                      | ( GREQ[binexp.op = PRISM_OP_GREQ] >> numexp[dtmc.res = construct_<prism_ast_binexpr>(binexp.op, binexp.left, dtmc.res)]) 
                      | ( LTEQ[binexp.op = PRISM_OP_LTEQ] >> numexp[dtmc.res = construct_<prism_ast_binexpr>(binexp.op, binexp.left, dtmc.res)]) 
                      | ( GR[binexp.op = PRISM_OP_GR]  >> numexp[dtmc.res= construct_<prism_ast_binexpr>(binexp.op, binexp.left, dtmc.res)]) 
                      | ( LT[binexp.op = PRISM_OP_LT]  >> numexp[dtmc.res = construct_<prism_ast_binexpr>(binexp.op, binexp.left, dtmc.res)]))
    		;
    			
    		numexp
    		=   sum [numexp.left = dtmc.res]
                    >> !(( PLUS[numexp.op = PRISM_OP_PLUS] 
                          >> numexp[dtmc.res = construct_<prism_ast_binexpr>(numexp.op, numexp.left, dtmc.res)]
                          ) 
                    |   ( MINUS[numexp.op = PRISM_OP_MINUS]
                          >> numexp[dtmc.res = construct_<prism_ast_binexpr>(numexp.op, numexp.left, dtmc.res)]
                          )
                    )
    		;
    						
    		sum
    		=   value[sum.left = dtmc.res]
                    >>  !( ( MULT[sum.op = PRISM_OP_MULT]
                            >> sum[dtmc.res = construct_<prism_ast_binexpr>(sum.op, sum.left, dtmc.res)]
                            )
                        | ( DIV[sum.op = PRISM_OP_DIV]
                            >> sum[dtmc.res = construct_<prism_ast_binexpr>(sum.op, sum.left, dtmc.res)]
                            )
                         )
    		;
    			
    		value
    		=       ident_p[dtmc.res = construct_<prism_ast_expr>(arg1)]
                    |   const_p[dtmc.res = construct_<prism_ast_expr>(arg1)]
                    |   ( no_node_d[LPAR] >> numexp >> no_node_d[RPAR] ) 
    		;
                
                formula_def 
                =   FORMULA >> ident_p[formula_def.name = arg1] >> EQ >> expression[push_back(dtmc.form, construct_<prism_ast_formula>(formula_def.name, dtmc.res))] >> SEMICOLON;
                
            BOOST_SPIRIT_DEBUG_RULE(value);
            BOOST_SPIRIT_DEBUG_RULE(sum);
            BOOST_SPIRIT_DEBUG_RULE(binexp);
            BOOST_SPIRIT_DEBUG_RULE(binexpand);
            BOOST_SPIRIT_DEBUG_RULE(binexpor);
            BOOST_SPIRIT_DEBUG_RULE(expression);
            BOOST_SPIRIT_DEBUG_RULE(probupdate);
            BOOST_SPIRIT_DEBUG_RULE(update);
            BOOST_SPIRIT_DEBUG_RULE(updates);
            BOOST_SPIRIT_DEBUG_RULE(transition_def);
            BOOST_SPIRIT_DEBUG_RULE(variable_def);
            BOOST_SPIRIT_DEBUG_RULE(module_def);
    	}

        rule<ScannerT, binexp_closure::context_t, parser_tag<0> > expression, numexp, sum, binexp;
        rule<ScannerT, update_closure::context_t, parser_tag<0> > update;
        rule<ScannerT, updates_closure::context_t, parser_tag<0> > updates;
        rule<ScannerT, transition_closure::context_t, parser_tag<0> > transition_def;
        rule<ScannerT, variable_closure::context_t, parser_tag<0> > variable_def, formula_def;
        rule<ScannerT, module_closure::context_t, parser_tag<0> > module_def;
        rule<ScannerT, dtmc_closure::context_t, parser_tag<0> > dtmc;
        
        rule<ScannerT> value, sysmodule;
        
        token_p<token*> MODULE, ENDMODULE, INIT, CONST, COLON, LBRAKET, RBRAKET, ENDINIT,
                      DOTS, BOOL, SEMICOLON, ARROW, AND, PRIME, EQ, NEQ, OR, 
                      NOT, LT, GR, GREQ, LTEQ, PLUS, MINUS, MULT, DIV, TRUE, LPAR, RPAR,
                      SYSTEM, ENDSYSTEM, FORMULA, BAR;
        
        rule<ScannerT, dtmc_closure::context_t, parser_tag<0> > const&
        start() const { return dtmc; }
            
        };
    
    Actions& m_actions;
};

#endif	/* _prism_parser_H */

